0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 77 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 16 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 7 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 PiDPToQDPProof (⇒, 0 ms)
↳16 QDP
↳17 QDPOrderProof (⇔, 57 ms)
↳18 QDP
↳19 DependencyGraphProof (⇔, 0 ms)
↳20 TRUE
TRANSPOSED_IN_AG(cons(X1, X2), cons(X3, X4)) → U5_AG(X1, X2, X3, X4, pB_in_aggaaa(X1, X3, X4, X5, X6, X2))
TRANSPOSED_IN_AG(cons(X1, X2), cons(X3, X4)) → PB_IN_AGGAAA(X1, X3, X4, X5, X6, X2)
PB_IN_AGGAAA(cons(X1, X2), cons(X1, X3), X4, cons(X3, X5), cons(nil, X6), X7) → U2_AGGAAA(X1, X2, X3, X4, X5, X6, X7, row2colA_in_agaa(X2, X4, X5, X6))
PB_IN_AGGAAA(cons(X1, X2), cons(X1, X3), X4, cons(X3, X5), cons(nil, X6), X7) → ROW2COLA_IN_AGAA(X2, X4, X5, X6)
ROW2COLA_IN_AGAA(cons(X1, X2), cons(cons(X1, X3), X4), cons(X3, X5), cons(nil, X6)) → U1_AGAA(X1, X2, X3, X4, X5, X6, row2colA_in_agaa(X2, X4, X5, X6))
ROW2COLA_IN_AGAA(cons(X1, X2), cons(cons(X1, X3), X4), cons(X3, X5), cons(nil, X6)) → ROW2COLA_IN_AGAA(X2, X4, X5, X6)
PB_IN_AGGAAA(X1, X2, X3, cons(X4, X5), X6, cons(X7, X8)) → U3_AGGAAA(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_in_aggaa(X1, X2, X3, cons(X4, X5), X6))
U3_AGGAAA(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_out_aggaa(X1, X2, X3, cons(X4, X5), X6)) → U4_AGGAAA(X1, X2, X3, X4, X5, X6, X7, X8, pB_in_aggaaa(X7, X4, X5, X9, X10, X8))
U3_AGGAAA(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_out_aggaa(X1, X2, X3, cons(X4, X5), X6)) → PB_IN_AGGAAA(X7, X4, X5, X9, X10, X8)
row2colcC_in_aggaa(cons(X1, X2), cons(X1, X3), X4, cons(X3, X5), cons(nil, X6)) → U11_aggaa(X1, X2, X3, X4, X5, X6, row2colcA_in_agaa(X2, X4, X5, X6))
row2colcA_in_agaa(cons(X1, X2), cons(cons(X1, X3), X4), cons(X3, X5), cons(nil, X6)) → U7_agaa(X1, X2, X3, X4, X5, X6, row2colcA_in_agaa(X2, X4, X5, X6))
row2colcA_in_agaa(nil, nil, nil, nil) → row2colcA_out_agaa(nil, nil, nil, nil)
U7_agaa(X1, X2, X3, X4, X5, X6, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcA_out_agaa(cons(X1, X2), cons(cons(X1, X3), X4), cons(X3, X5), cons(nil, X6))
U11_aggaa(X1, X2, X3, X4, X5, X6, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcC_out_aggaa(cons(X1, X2), cons(X1, X3), X4, cons(X3, X5), cons(nil, X6))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
TRANSPOSED_IN_AG(cons(X1, X2), cons(X3, X4)) → U5_AG(X1, X2, X3, X4, pB_in_aggaaa(X1, X3, X4, X5, X6, X2))
TRANSPOSED_IN_AG(cons(X1, X2), cons(X3, X4)) → PB_IN_AGGAAA(X1, X3, X4, X5, X6, X2)
PB_IN_AGGAAA(cons(X1, X2), cons(X1, X3), X4, cons(X3, X5), cons(nil, X6), X7) → U2_AGGAAA(X1, X2, X3, X4, X5, X6, X7, row2colA_in_agaa(X2, X4, X5, X6))
PB_IN_AGGAAA(cons(X1, X2), cons(X1, X3), X4, cons(X3, X5), cons(nil, X6), X7) → ROW2COLA_IN_AGAA(X2, X4, X5, X6)
ROW2COLA_IN_AGAA(cons(X1, X2), cons(cons(X1, X3), X4), cons(X3, X5), cons(nil, X6)) → U1_AGAA(X1, X2, X3, X4, X5, X6, row2colA_in_agaa(X2, X4, X5, X6))
ROW2COLA_IN_AGAA(cons(X1, X2), cons(cons(X1, X3), X4), cons(X3, X5), cons(nil, X6)) → ROW2COLA_IN_AGAA(X2, X4, X5, X6)
PB_IN_AGGAAA(X1, X2, X3, cons(X4, X5), X6, cons(X7, X8)) → U3_AGGAAA(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_in_aggaa(X1, X2, X3, cons(X4, X5), X6))
U3_AGGAAA(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_out_aggaa(X1, X2, X3, cons(X4, X5), X6)) → U4_AGGAAA(X1, X2, X3, X4, X5, X6, X7, X8, pB_in_aggaaa(X7, X4, X5, X9, X10, X8))
U3_AGGAAA(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_out_aggaa(X1, X2, X3, cons(X4, X5), X6)) → PB_IN_AGGAAA(X7, X4, X5, X9, X10, X8)
row2colcC_in_aggaa(cons(X1, X2), cons(X1, X3), X4, cons(X3, X5), cons(nil, X6)) → U11_aggaa(X1, X2, X3, X4, X5, X6, row2colcA_in_agaa(X2, X4, X5, X6))
row2colcA_in_agaa(cons(X1, X2), cons(cons(X1, X3), X4), cons(X3, X5), cons(nil, X6)) → U7_agaa(X1, X2, X3, X4, X5, X6, row2colcA_in_agaa(X2, X4, X5, X6))
row2colcA_in_agaa(nil, nil, nil, nil) → row2colcA_out_agaa(nil, nil, nil, nil)
U7_agaa(X1, X2, X3, X4, X5, X6, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcA_out_agaa(cons(X1, X2), cons(cons(X1, X3), X4), cons(X3, X5), cons(nil, X6))
U11_aggaa(X1, X2, X3, X4, X5, X6, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcC_out_aggaa(cons(X1, X2), cons(X1, X3), X4, cons(X3, X5), cons(nil, X6))
ROW2COLA_IN_AGAA(cons(X1, X2), cons(cons(X1, X3), X4), cons(X3, X5), cons(nil, X6)) → ROW2COLA_IN_AGAA(X2, X4, X5, X6)
row2colcC_in_aggaa(cons(X1, X2), cons(X1, X3), X4, cons(X3, X5), cons(nil, X6)) → U11_aggaa(X1, X2, X3, X4, X5, X6, row2colcA_in_agaa(X2, X4, X5, X6))
row2colcA_in_agaa(cons(X1, X2), cons(cons(X1, X3), X4), cons(X3, X5), cons(nil, X6)) → U7_agaa(X1, X2, X3, X4, X5, X6, row2colcA_in_agaa(X2, X4, X5, X6))
row2colcA_in_agaa(nil, nil, nil, nil) → row2colcA_out_agaa(nil, nil, nil, nil)
U7_agaa(X1, X2, X3, X4, X5, X6, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcA_out_agaa(cons(X1, X2), cons(cons(X1, X3), X4), cons(X3, X5), cons(nil, X6))
U11_aggaa(X1, X2, X3, X4, X5, X6, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcC_out_aggaa(cons(X1, X2), cons(X1, X3), X4, cons(X3, X5), cons(nil, X6))
ROW2COLA_IN_AGAA(cons(X1, X2), cons(cons(X1, X3), X4), cons(X3, X5), cons(nil, X6)) → ROW2COLA_IN_AGAA(X2, X4, X5, X6)
ROW2COLA_IN_AGAA(cons(cons(X1, X3), X4)) → ROW2COLA_IN_AGAA(X4)
From the DPs we obtained the following set of size-change graphs:
PB_IN_AGGAAA(X1, X2, X3, cons(X4, X5), X6, cons(X7, X8)) → U3_AGGAAA(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_in_aggaa(X1, X2, X3, cons(X4, X5), X6))
U3_AGGAAA(X1, X2, X3, X4, X5, X6, X7, X8, row2colcC_out_aggaa(X1, X2, X3, cons(X4, X5), X6)) → PB_IN_AGGAAA(X7, X4, X5, X9, X10, X8)
row2colcC_in_aggaa(cons(X1, X2), cons(X1, X3), X4, cons(X3, X5), cons(nil, X6)) → U11_aggaa(X1, X2, X3, X4, X5, X6, row2colcA_in_agaa(X2, X4, X5, X6))
row2colcA_in_agaa(cons(X1, X2), cons(cons(X1, X3), X4), cons(X3, X5), cons(nil, X6)) → U7_agaa(X1, X2, X3, X4, X5, X6, row2colcA_in_agaa(X2, X4, X5, X6))
row2colcA_in_agaa(nil, nil, nil, nil) → row2colcA_out_agaa(nil, nil, nil, nil)
U7_agaa(X1, X2, X3, X4, X5, X6, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcA_out_agaa(cons(X1, X2), cons(cons(X1, X3), X4), cons(X3, X5), cons(nil, X6))
U11_aggaa(X1, X2, X3, X4, X5, X6, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcC_out_aggaa(cons(X1, X2), cons(X1, X3), X4, cons(X3, X5), cons(nil, X6))
PB_IN_AGGAAA(X2, X3) → U3_AGGAAA(X2, X3, row2colcC_in_aggaa(X2, X3))
U3_AGGAAA(X2, X3, row2colcC_out_aggaa(X1, X2, X3, cons(X4, X5), X6)) → PB_IN_AGGAAA(X4, X5)
row2colcC_in_aggaa(cons(X1, X3), X4) → U11_aggaa(X1, X3, X4, row2colcA_in_agaa(X4))
row2colcA_in_agaa(cons(cons(X1, X3), X4)) → U7_agaa(X1, X3, X4, row2colcA_in_agaa(X4))
row2colcA_in_agaa(nil) → row2colcA_out_agaa(nil, nil, nil, nil)
U7_agaa(X1, X3, X4, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcA_out_agaa(cons(X1, X2), cons(cons(X1, X3), X4), cons(X3, X5), cons(nil, X6))
U11_aggaa(X1, X3, X4, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcC_out_aggaa(cons(X1, X2), cons(X1, X3), X4, cons(X3, X5), cons(nil, X6))
row2colcC_in_aggaa(x0, x1)
row2colcA_in_agaa(x0)
U7_agaa(x0, x1, x2, x3)
U11_aggaa(x0, x1, x2, x3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PB_IN_AGGAAA(X2, X3) → U3_AGGAAA(X2, X3, row2colcC_in_aggaa(X2, X3))
POL(PB_IN_AGGAAA(x1, x2)) = 1 + x1 + x2
POL(U11_aggaa(x1, x2, x3, x4)) = 1 + x2 + x4
POL(U3_AGGAAA(x1, x2, x3)) = x3
POL(U7_agaa(x1, x2, x3, x4)) = 1 + x2 + x4
POL(cons(x1, x2)) = 1 + x1 + x2
POL(nil) = 0
POL(row2colcA_in_agaa(x1)) = x1
POL(row2colcA_out_agaa(x1, x2, x3, x4)) = x3
POL(row2colcC_in_aggaa(x1, x2)) = x1 + x2
POL(row2colcC_out_aggaa(x1, x2, x3, x4, x5)) = x4
row2colcC_in_aggaa(cons(X1, X3), X4) → U11_aggaa(X1, X3, X4, row2colcA_in_agaa(X4))
row2colcA_in_agaa(cons(cons(X1, X3), X4)) → U7_agaa(X1, X3, X4, row2colcA_in_agaa(X4))
row2colcA_in_agaa(nil) → row2colcA_out_agaa(nil, nil, nil, nil)
U11_aggaa(X1, X3, X4, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcC_out_aggaa(cons(X1, X2), cons(X1, X3), X4, cons(X3, X5), cons(nil, X6))
U7_agaa(X1, X3, X4, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcA_out_agaa(cons(X1, X2), cons(cons(X1, X3), X4), cons(X3, X5), cons(nil, X6))
U3_AGGAAA(X2, X3, row2colcC_out_aggaa(X1, X2, X3, cons(X4, X5), X6)) → PB_IN_AGGAAA(X4, X5)
row2colcC_in_aggaa(cons(X1, X3), X4) → U11_aggaa(X1, X3, X4, row2colcA_in_agaa(X4))
row2colcA_in_agaa(cons(cons(X1, X3), X4)) → U7_agaa(X1, X3, X4, row2colcA_in_agaa(X4))
row2colcA_in_agaa(nil) → row2colcA_out_agaa(nil, nil, nil, nil)
U7_agaa(X1, X3, X4, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcA_out_agaa(cons(X1, X2), cons(cons(X1, X3), X4), cons(X3, X5), cons(nil, X6))
U11_aggaa(X1, X3, X4, row2colcA_out_agaa(X2, X4, X5, X6)) → row2colcC_out_aggaa(cons(X1, X2), cons(X1, X3), X4, cons(X3, X5), cons(nil, X6))
row2colcC_in_aggaa(x0, x1)
row2colcA_in_agaa(x0)
U7_agaa(x0, x1, x2, x3)
U11_aggaa(x0, x1, x2, x3)